Nuprl Lemma : adjacent-to-same 11,40
T:Type, L:(T List), a, b, c:T.
no_repeats(T;L)  adjacent(T;L;a;b)  adjacent(T;L;a;c)  (b = c) 
latex

Definitionss = t, x:AB(x), x:A. B(x), Type, type List, no_repeats(T;l), adjacent(T;L;x;y), left + right, P  Q, x before y  l, P  Q, t  T, False, A
Lemmasl before antisymmetry, adjacent-before, adjacent wf, no repeats wf, before-adjacent2, l before wf

origin